Nuprl Definition : l-ordered
11,40
postcript
pdf
l-ordered(
T
;
x
,
y
.
R
(
x
;
y
);
L
) ==
x
,
y
:
T
. l_before(
x
;
y
;
L
;
T
)
R
(
x
;
y
)
latex
clarification:
l-ordered(
T
;
x
,
y
.
R
(
x
;
y
);
L
) ==
x
:
T
,
y
:
T
. l_before(
x
;
y
;
L
;
T
)
R
(
x
;
y
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
l_before(
x
;
y
;
l
;
T
)
FDL editor aliases
l-ordered
origin